Skip to content

Expose missing native propagators through MiniZinc and FlatZinc - #253

Draft
zayenz wants to merge 19 commits into
feature/inter-distancefrom
feature/minizinc-registry
Draft

zayenz wants to merge 19 commits into
feature/inter-distancefrom
feature/minizinc-registry

Conversation

@zayenz

@zayenz zayenz commented Oct 10, 2026 •

Copy link
Copy Markdown
Member

Several MiniZinc relations still use decompositions despite matching Gecode propagators. This PR connects those propagators through standard fzn_ hooks and provides explicit modelling predicates for native constraints without a suitable standard hook.

Standard globals keep MiniZinc's public overloads, assertions, index handling and optional-value translations. The solver library overrides the typed hooks for count inequalities, conditionals, nondeterministic regular, optional distinctness and scheduling, and set intersection. Low-level builtin redefinitions handle set/float extrema, float powers, set matrix element and scalar implication. The public overrides in solver-native-overloads.mzn are removed.

gecode.mzn contains documented modelling interfaces for offset distinctness, array inequality, arbitrary-tie sorting and extrema, NValues/among/matching-count bounds, native arithmetic and products, distance constraints, optional successor paths, optional rectangles and additional set relations. The interfaces lower enums and array indexes to typed FlatZinc bindings in gecode_fzn.mzn. Paths use absent terminal successors, and rectangle origins encode absence together. Reification uses native forms or standard decompositions where available; unsupported forms are documented. Duplicate standard globals, sparse GCC, task-type dispatch and generic relation/operation-code APIs are removed.

Annotations select basic, advanced or combined propagation and single or pairwise minimum-distance actors. Fixed-base float powers and inverse logarithms use explicit MPFR rounding; compiler rounding flags match the parent branch. Divmod bounds are available before dependent linear constraints are posted. General variable-base/variable-exponent float powers remain unsupported.

The interface review also fixed present integer path successors being mistaken for the native terminal marker, a rectangle primitive shadowing the modelling overload, and exceptions for fixed negative inter-distance values. Negative distances now fail consistently with the variable form.

GitHub stack #254: #249 → #247 → #253. This draft is based on #247 (feature/inter-distance).

Validation of the revised library:

  • Built fzn-gecode and gecode-test; all 137 FlatZinc regressions passed.
  • All 136 MiniZinc integration cases passed: 55 standard routing cases, 16 standard optional/NFA/product cases and 65 native modelling API cases. Coverage includes root/reified/implied relations, enums, shifted indexes, absence, empty arrays, terminal costs, strict zero-size rectangles and propagation annotations.
  • Used local Zincite at f950541 on all 28 edited MiniZinc files or added sections. Checked parsing, tokens, comments and formatter second-pass stability; preserved include order and existing untouched prefixes. Manually corrected fitting quantified condition chains and conditional comprehensions. Local Zincite tasks base-102 and base-103 record these layout problems.
  • MiniZinc predicate documentation generation, changelog checks and whitespace checks passed. The earlier float implementation passed 73 transcendental regressions; it is unchanged by this library reorganization.

The Challenge measurements below are historical results from earlier PR iterations. They preceded restoration of the parent compiler flags, the local MPFR correction and this library reorganization. They do not establish performance of the final interfaces or float implementation.

MiniZinc Challenge validation (corpus a8448864fc56162583f24aaf9c25653d93f83765, MiniZinc 2.10.1):

  • Compiled 350 of 363 distinct model/include groups against both parent and PR libraries after recorded historical compatibility repairs. The remaining 13 have missing inputs or old source incompatibilities; none fails only on the PR.
  • Tested one structurally small official instance for each of 48 models whose flattened constraints select modified routes, plus five conservative controls, using a five-second search limit. No automatic-route solver errors or invalid final assignments were observed. Some cases reach the time limit without an incumbent.
  • Eight models received three paired follow-up runs with a ten-second search limit and six solver threads. Median completed solve times improved for compression (4.427 to 4.000 s), valve-network (5.703 to 5.178 s), and 2014 liner fm3_11 (4.455 to 4.093 s). 2019 liner fm3_3 increased from 2.645 to 2.917 s, with overlapping ranges. All completed pairs proved the same optimum. These small, parallel samples do not establish a general speedup.
  • Tested six explicit native formulations: nvalues in physician scheduling, steel-mill slabs and peaceable queens; set at-most-one in Steiner systems; set-target count in Unison; joint divmod in rotating workforce. They exposed the divmod bound issue, now fixed; all six original/native workforce follow-up runs returned checked solutions. No clear formulation speedup was established, and steel-mill nvalues produced worse incumbents.
  • The divmod MiniZinc facade also passed exhaustive checking of all 66 signed dividend/divisor tuples in the selected small domains. Final assignments were pinned as equality constraints in fresh compilations of the original models, preserving declared domains and ub/lb semantics.

@zayenz
zayenz added this pull request to stack #254 October 10, 2026 18:20

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant